package HeapArray;

/*KORAT_START*/
/*KORAT_END*/
public class HeapArray{
    private /*KORAT_START*//*@ spec_public @*//*KORAT_END*/int size; // number of elements in the heap
    private /*KORAT_START*//*@ spec_public @*//*KORAT_END*/Comparable[] array; // heap elements     
    /*@ public normal_behavior
      @     requires repOk() && size > 0;
      @     ensures repOk() && \result == \old(array[0]);
      @ also public exceptional_behavior
      @     requires repOk() && size == 0;
      @     signals (IllegalArgumentException e) true;
      @*/
    public Object extractMax() {
        if (size == 0) 
            throw new IllegalArgumentException();
        Object o = array[0];
        array[0] = array[--size];
        array[size] = null;
        heapifyDown(0);
        return o;
    }
    
    private void heapifyDown(int index){
        int son;
        Comparable elm = array[index];
        son = index * 2 + 1;
        if ((son + 1 < size) && (array[son].compareTo(array[son + 1]) < 0)) son = son + 1;
        while ((son < size) && (elm.compareTo(array[son]) < 0)) {
            array[index] = array[son];
            index = son;
            son = son * 2 + 1;
            if ((son + 1 < size) && (array[son].compareTo(array[son + 1]) < 0)) son = son + 1;
            if (son >= size) break;
        }
        array[index] = elm;
    }

    /*@ public normal_behavior
      @     requires repOk();
      @     ensures repOk();
      @*/
    public boolean insert(Comparable element) {
        /*
        if (element == null)
            return false;
        */

        if (size >= array.length) { // then double the length of the array (=> O(1) amortized cost ;)
            Comparable temp[] = new Comparable[2*array.length+1];
            for(int i = 0; i < size; i++)
                temp[i] = array[i];
            array = temp;
        }
        
        array[size] = element;
        heapifyUp(size);
        size++;
        return true;
    }

    private void heapifyUp(int index) {
        while (index > 0 && array[(index-1) / 2].compareTo(array[index]) < 0) {
            Comparable t = array[index];
            array[index] = array[(index-1) / 2];
            array[(index-1) / 2] = t;
            index = (index-1) / 2;
        }
    }
    /*KORAT_END*/
    /*KORAT_START*/
    
    public HeapArray() { array = new Integer[5]; }
}